Issue2024-record.agda:3,15-18
Not in scope:
  Foo at Issue2024-record.agda:3,15-18
when scope checking Foo
